Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Updated Docker CI workflow #1227

Merged
merged 5 commits into from
May 3, 2024
Merged

Conversation

binghe
Copy link
Member

@binghe binghe commented Apr 25, 2024

Hi,

I updated the Docker CI workflows with the following changes:

  • Now HOL manuals will be built after HOL itself (only with PolyML). The related docker images have been updated with some additional TeXlive packages.
  • In addition to the existing stdknl and expk builds using PolyML. Now for each new commit and PR, the CI workflow also contains a basic expk build using Moscow ML. The command line option is --expk --seq=tools/sequences/upto-parallel -t, which can finish in about 35 minutes.
  • I installed new versions of Z3 SMT solver (4.13.0), which is also used by default. (The previous version (4.12.x) is still there.)

P. S. The current building errors with Moscow ML is in cv-related code after boss, thus the newly added CI tests cannot expose it. I look forward for an enriched build sequence (no parallelisation) which can extend the related CI tests to 1-1.5 hours with more theories covered.

Chun

@binghe
Copy link
Member Author

binghe commented Apr 25, 2024

I've pushed a new commit to fix the build with Moscow ML (#1226).

@binghe
Copy link
Member Author

binghe commented Apr 30, 2024

The last commit fixed manual building inside CI workflow (previously due to bash script grammar errors the manuals were not built).

@mn200
Copy link
Member

mn200 commented May 3, 2024

Fantastic; thank you!

@mn200 mn200 merged commit 4387c34 into HOL-Theorem-Prover:develop May 3, 2024
3 checks passed
@binghe binghe deleted the docker-ci.mosml branch May 3, 2024 03:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants